COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	ARPA report
C00007 ENDMK
C⊗;
ARPA report

	John McCarthy continued his work in formalization
of the common sense facts about the world needed for intelligent
behavior and also work in formalization of computer programs.
This work led to the following reports and publications:

1. Two papers with R.S. Cartwright on the representation of recursive
programs in first order logic were published in POPL conferences.

2. In Spring 1979 McCarthy discovered
a formalism for representing sequential programs
in first order logic now called Elephant - it never forgets.
Unlike previous formalisms, Elephant uses time explicitly as
an independent variable and a program counter as an explicit
function of time.  As a result, properties of programs
can be proved directly from the program and the axiomatization
of the data domain.  Besides that, Elephant programs can refer
directly to past inputs and events - sometimes obviating the
need for the programmer to define certain data structures for
remembering these events; the data structures are then supplied
by the compiler.  In this one respect
Elephant is a higher level language
then any developed so far.

3. Work continued on formalisms for representing knowledge.
Ma Xiwen revised McCarthy's set of axioms for representing the
rather difficult knowledge puzzle of Mr. S and Mr. P and used
FOL to verify the translation of the knowledge problem to
a purely arithmetic problem.
This work is part a study of the representation of facts about
knowledge that will aid the development of programs that
know what people and other programs do and don't know.

4. McCarthy further developed his method called circumscription of
non-monotonic reasoning and related it to the methods developed by
Raymond Reiter and by Drew McDermott and Jon Doyle jointly.
It turns out that humans do non-monotonic reasoning all the time,
and machines must do it in order to behave intelligently.  In
our opinion, the formalization of non-monotonic reasoning is
a major theoretical step preparing for practical AI systems
that can avoid excessively specialized formulations of their
knowledge of the world.

	A conference on non-monotonic reasoning was held at Stanford
in November 1978, and its proceedings are being published as a
special issue of the journal %2Artificial Intelligence%1.

	Carolyn Talcott continued her studies in preparation
for writing a dissertation that will combine the methods of recursive
function theory with the programming techniques of LISP.
Hopefully, it will permit the formulation and proof
of more complex facts about more complex programs.

	Weyhrauch
	Goad
	Brooks